Some computing systems may be used for formal verification, for example, proving or disproving the correctness of an intended algorithm underlying a hardware and/or software system with respect to a formal specification or properties. Formal verification may be performed, for example, using a Model Checking Algorithm (MCA) which checks substantially all states and transitions in an abstract model of the system.
Some models may be very large, and may include hundreds of thousands of elements. Checking a large model may be time consuming and may require significant computational resources (e.g., processing resources and/or memory resources). Therefore, a Model-Reduction Algorithm (MRA) may be used prior to model checking, in order to reduce the size and/or the complexity of the model to be checked. The output of the MRA may be a reduced model, having the same functionality yet decreased size and/or complexity.
Unfortunately, running a MRA may be time consuming and may require significant computational resources. Accordingly, there is a trade-off between running a MRA to reduce the model and running a MCA to check the model, since longer model-reduction may, or may not, lead to shorter model-checking. Therefore, efforts are being made by users of formal verification systems reduce the total time of both model-checking and model-reduction algorithms, for example, by speculating whether or not it would be beneficial (e.g., time-saving) to run one or more MRAs prior to running a MCA. However, the user may not be able to determine how much time to allocate to model reduction prior to commencing the model checking. For example, it may not necessarily be beneficial to execute a MRA for a long period of time, or to execute multiple MRAs, unless such MRA(s) will result in significant savings of resources for the overall formal verification process.
In particular, it may be difficult to predict in advance the effectiveness of a MRA; for example, in some cases, a long runtime of a particular MRA may not justify the relatively small reduction in model size or complexity, and thus may not reduce the MCA runtime, and may even increase the overall formal verification runtime. Additionally, in some cases, it may not be beneficial to execute a MRA because a particular model may be checked relatively quickly without, or with minimal, model reduction efforts.
Some computing systems may utilize transformation-based formal verification, in which model reduction and model checking are interleaved. For example, in some systems, a basic MRA may be initially executed; upon termination of the execution of the MRA, one or more MCAs may be executed; if the one or more MCAs fail to provide a solution to all problems in the partially-reduced model, then, upon the termination of the execution of these MCAs, an advanced (e.g., computationally intensive) MRA is executed, in an attempt to further reduce the model. Upon the termination of the execution of the advanced MRA, one or more MCAs may be executed; and so forth. The model reduction efforts may be repeatedly escalated, interleaved with the model checking efforts, until the model is formally verified. In other computing systems, multiple MCAs are executed in parallel, and may be terminated as soon as one of the MCAs verifies the model.